T:Type, Q:((T List)Prop).
Q(nil)
 (x:T. Q([x]))
 (ys, ys':T List. Q(ys)  Q(ys')  Q(ys @ ys'))
 {zs:T List. Q(zs)} 

latex

Definitions	t  T, Prop, x(s), x:A. B(x), as @ bs, P  Q, {T}
Lemmas	append wf